Nuprl Lemma : all_functionality_wrt_iff
9,38
postcript
pdf
S
,
T
:Type,
P
,
Q
:(
S
). (
S
=
T
)
(
x
:
S
.
P
(
x
)
Q
(
x
))
((
x
:
S
.
P
(
x
))
(
y
:
T
.
Q
(
y
)))
latex
ProofTree
Definitions
P
Q
,
P
Q
,
P
Q
,
t
T
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
iff
wf
origin
S,T:Type, P,Q:(S
). (S = T) 
(x:S. P(x) 
Q(x)) ((x:S. P(x)) (y:T. Q(y)))
S,T:Type, P,Q:(S). (S = T) (x:S. P(x) Q(x)) ((x:S. P(x)) (y:T. Q(y)))
Q Q
Q
T Qx:A. B(x)